$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]SWellFounded($R$($x$,$y$))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. Dec($\exists$$z$:$T$. ($R$($x$,$z$) \& $R$($z$,$y$))))
\\[0ex]$\Rightarrow$ ($\forall$$y$:$T$. ($\exists$$x$:$T$. ($R$($x$,$y$))) $\Rightarrow$ ($\exists$$x$:$T$. ($R$!($x$,$y$))))